from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)
↳ QTRS
↳ DependencyPairsProof
from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)
LENGTH(cons(X, Y)) → LENGTH1(Y)
LENGTH1(X) → LENGTH(X)
FROM(X) → FROM(s(X))
from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
LENGTH(cons(X, Y)) → LENGTH1(Y)
LENGTH1(X) → LENGTH(X)
FROM(X) → FROM(s(X))
from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
LENGTH(cons(X, Y)) → LENGTH1(Y)
LENGTH1(X) → LENGTH(X)
from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LENGTH(cons(X, Y)) → LENGTH1(Y)
LENGTH1(X) → LENGTH(X)
The value of delta used in the strict ordering is 3/4.
POL(LENGTH(x1)) = 7/4 + x_1
POL(cons(x1, x2)) = 9/4 + (4)x_2
POL(LENGTH1(x1)) = 5/2 + (13/4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
FROM(X) → FROM(s(X))
from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)